Inference at * 
Iof proof for Lemma fun thru spread:


  A:Type, B:(AType), p:(x:A  B(x)), C,D:Type, f:(CD), b:(x:AB(x)C).
  f(let x,y = p in b(x,y)) = let x,y = p in f(b(x,y)) 

latex

 by ((UnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : AType
C1: 3. p : x:A  B(x)
C1: 4. C : Type
C1: 5. D : Type
C1: 6. f : CD
C1: 7. b : x:AB(x)C
C1:   f(let x,y = p in b(x,y)) = let x,y = p in f(b(x,y))
C.

Definitions

t  T, x(s), x:A. B(x)